\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $E$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$
\\[0ex]3. \=$\downarrow$(($\forall$$a$:$T$. $E$($a$,$a$))\+
\\[0ex]\& ($\forall$$a$, $b$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$a$))
\\[0ex]\& ($\forall$$a$, $b$, $c$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$c$) $\Rightarrow$ $E$($a$,$c$)))
\-\\[0ex]4. $a$ : $T$
\\[0ex]5. $b$ : $T$
\\[0ex]6. $\downarrow$$E$($a$,$b$)
\\[0ex]$\vdash$  $\downarrow$$E$($b$,$a$)
\end{tabbing}